enrich
   int-array
with
   

   
   
   functions  sum : int-array × nat × nat → int;
   predicates  maximum-sum : int-array × int;
               upper-bound : int-array × int;
               suffix-upper-bound : int-array × int;
               maximum-sum : int-array × nat × nat × int;
               maximum-suffix-sum : int-array × nat × int;
   
   
   
   

   

   axioms sum-zero :  ⊦ sum(ar, n, 0) = 0;
          used for: s, ls;
          sum-succ : n + m < # ar ⊦ sum(ar, n, m + 1) = sum(ar, n, m) + ar[n + m];
          used for: s, ls;
          maximum-sum :  ⊦ maximum-sum(ar, i) ↔ (∃ n, m. n + m ≤ # ar ∧ maximum-sum(ar, n, m, i));
          used for: s, ls;
          maximum-sum-bounds :  ⊦ maximum-sum(ar, n, m, i) ↔ n + m ≤ # ar ∧ i = sum(ar, n, m) ∧ upper-bound(ar, i);
          used for: ls;
          upper-bound :  ⊦ upper-bound(ar, i) ↔ (∀ n, m. n + m ≤ # ar → sum(ar, n, m) ≤ i);
          used for: ls;
          maximum-suffix-sum :  ⊦ maximum-suffix-sum(ar, n, i) ↔ n ≤ # ar ∧ i = sum(ar, n, # ar - n) ∧ suffix-upper-bound(ar, i);
          used for: ls;
          suffix-upper-bound :  ⊦ suffix-upper-bound(ar, i) ↔ (∀ n. n ≤ # ar → sum(ar, n, # ar - n) ≤ i);
          used for: ls;

   

   
end enrich